MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 18:57:15 GMT
Content-Type: text/html
Content-Length: 9558
Last-Modified: Thursday, 30-Nov-95 21:21:19 GMT

<html>
<head>
<title>Fred B. Schneider
</title>
</head>
<body>
<!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/People/fbs/fbs.gif">
<!WA1><!WA1><!WA1><!WA1><img align=left vspace=3 hspace=15 
src="http://www.cs.cornell.edu/Info/People/fbs/fbs-thumb.gif">
</a>
<h2>
Fred B. Schneider <br>
Professor<br>
PhD State Univ. of N.Y., Stony Brook, 1978
</h2>
<p>
<hr>
<p>

Techniques for understanding concurrent programs are becoming increasingly 
important as distributed computing systems become widespread in 
mission-critical applications.  My research has focused on the development 
of these techniques.
<p>
I have been heavily involved in applying assertional reasoning to the 
design of concurrent, distributed, fault-tolerant, and real-time programs.  
I am completing a textbook on this subject.  Along with David Gries, I 
continue investigations concerning our first-order equational logic E.  
This past year, we streamlined the inference rules and evaluated a number 
of techniques for handling undefined terms and partial functions.
<p>
Thomas Bressoud and I completed building and analyzing our hypervisor-based 
implementation of replication management for HP's PA-RISC architecture.  
Our protocols ensure that the sequence of instructions executed by two 
virtual machines running on different physical processors are identical.  
The protocols also coordinate I/O issued by these virtual machines.  Use of 
a hypervisor to implement replica coordination is attractive - at least, in 
theory.  When replica coordination is implemented in a hypervisor, it 
instantly becomes available to all hardware realizations of the given 
instruction-set architecture, including realizations that did not exist 
when the hypervisor was written.  Second, when replica coordination is 
implemented in a hypervisor, a single implementation suffices for every 
operating system that executes on that instruction-set architecture.  
Finally, by implementing replica coordination in a hypervisor, the 
applications programmer is freed from this task.
<p>
Jointly with Dag Johansen (University of Troms&oslash;, Norway) and Robbert van 
Renesse, I started the TACOMA project (Troms&oslash; And COrnell Moving Agents) to 
investigate support and use of mobile processes in building 
mission-critical applications.  By structuring a system in terms of agents, 
applications can be constructed in which communication-network bandwidth is 
conserved.  Data may be accessed only by an agent executing at the same 
site as the data resides.  An agent typically will filter or otherwise 
reduce the data it reads, carrying with it only the relevant information as 
it roams the network.  Two TACOMA prototypes have been completed, and we 
are implementing a third system based on our experiences.
<p>
Finally, I developed with Scott Stoller a new algorithm for detecting 
whether a particular computation of an asynchronous distributed system 
could have passed through a global state satisfying some given state 
predicate.  The new algorithm allows more efficient detection than is 
possible with previous algorithms.
<p>
<hr>

<H2>University Activities</H2>
<ul>
<li>Sabbatical leave, 1994-95
</ul>

<H2>Professional Activities</H2>
<ul>
<li>Editor-in-chief, <EM>Distributed Computing</EM>
<li>Editor, <EM>Information Processing Letters</EM>
<li>Editor, <EM>IEEE Transactions on Software Engineering</EM>
<li>Editor, <EM>High Integrity Systems</EM>
<li>Editor, <EM>Annals of Software Engineering</EM>
<li>Editor, <EM>ACM Computing Surveys</EM>
<li>Co-Editor, Texts and Monographs in Computer Science, Springer-Verlag
<li>Program Committee Member, 3rd International School and Symposium on 
	Formal Techniques in Real-Time and Fault-Tolerant Systems
<li>Program Committee Member, 3rd International Conference on the Mathematics 
	of Program Construction
<li>Program Committee Member, 4th International Workshop On Responsive 
	Computer Systems
<li>Program Committee Member, Workshop on Composability of Fault-resilient 
	Real-Time Systems
<li>Program Committee Member, Fifth IFIP Working Conference on Dependable 
	Computing for Critical Applications
<li>Program Committee Member, Sixteenth IEEE International Real-Time Systems 
	Symposium
<li>Program Committee Member, DIMACS Workshop on Verification and Control 
	of Hybrid Systems
<li>Steering committee, Center for High Integrity Software Systems 
	Assurance (CHISSA), National Institute of Standards and Technology
<li>Member, ISAT Defensive Information Warfare Study Group, Advanced Research 
	Projects Agency
<li>Review committee, Leibniz Center at Hebrew University
<li>Member, IFIP Working Group 2.3 (Programming Methodology)
</ul>

<H2>Awards</H2>
<ul>
<li>Fellow, American Association for Advancement of Science
<li>Fellow, Association for Computing Machinery
</ul>

<H2>Lectures</H2>
<ul>
<li>Proof outlines for programs. 6 lectures. 15th International Summer 
	School, Marktoberdorf, Germany, July 1994.
<li>On the origin of traditions. Banquet speech. 15th International Summer 
	School, Marktoberdorf, Germany, July 1994.
<li>Reasoning about programs by exploiting the environment. AFOSR 
	Grantees/Contractors Meeting In Software and Systems, Washington, 
	D.C., Sept. 1994.
<li>Verifying hybrid systems by exploiting the environment. Symposium on 
	Formal Techniques in Real-Time and Fault-Tolerant Systems. 
	Lubeck, Germany, Sept. 1994.
<li>Panelist: comparative merits of synchronous, partially synchronous, 
	and asynchronous models for safety-critical real-time systems. 
	Symposium on Formal Techniques in Real-Time and Fault-Tolerant 
	Systems. Lubeck, Germany, Sept. 1994.
<li>Moderator: issues in writing formal specifications. Specification and 
	Refinement of Reactive Systems. International Conference and Research 
	Center for Computer Science, Dagstuhl, Germany, Sept. 1994.
<li>Merging policies. Workshop on Computer Support for Policy Analysis and 
	Design. George Mason University, Virginia, Dec. 1994.
<li>Avoiding AAS mistakes. Invited speaker. Air Traffic Management Workshop, 
	NASA Ames Research Center, Feb. 1995.
<li>Reasoning about programs by exploiting the environment. Technical 
	University of Munich. Munich, Germany, Feb. 1995.
<li>Proof outlines of the past. University of North Carolina, Chapel Hill, 
	North Carolina, March 1995.
<li>Adding fault-tolerance, virtually. Distinguished Lecture Series, 
	University of North Carolina, Chapel Hill, North Carolina, March 1995.
<li>Moderator and panel organizer: teaching logic as tool. SIGCSE Technical 
	Symposium on Computer Science Education, Nashville, Tennessee, March 1995.
<li>Proof outlines of the past. Technion, Haifa, Israel, March 1995.
<li>Adding fault-tolerance, virtually. University of Troms&oslash;, Troms&oslash;, Norway, 
	April 1995.
<li>Concurrent programs from specifications. University of Troms&oslash;, Troms&oslash;, 
	Norway, April 1995.
<li>Placing agents on airplanes - a  view of AAS and its successor. ARPA ISAT 
	Defensive Information Warfare Study Group Meeting, Washington, D.C., 
	June 1995.
</ul>

<H2>Publications</H2>
<ul>
<li>Reasoning about programs by exploiting the environment.  <EM>Proceedings 21st 
	International Colloquium, ICALP'94</EM>   (Jerusalem, Israel, July 1994), 
	<EM>Lecture Notes in Computer Science 820,</EM> Springer-Verlag, New York, 
	328-339 (with L. Fix).
<li>Notes on proof outline logic. Working Material. 15th International Summer 
	School, Marktoberdorf, Germany, July 1994.
<li>Research on fault-tolerant and real-time computing. Software and Systems 
	Program Summary.   (Bolling Air Force Base, Washington D.C., Sept. 
	1994), Air Force Office of Scientific Research, 75-77.
<li>Hybrid verification by exploiting the environment.  <EM>Formal Techniques in 
	Real-Time and Fault-Tolerant Systems</EM>  (Lubeck, Germany, September 
	1994), <EM>Lecture Notes in Computer Science, Volume 863,</EM> Springer-Verlag, 
	New York, 1-18 (with Limor Fix).
<li>Equational propositional logic.  <EM>Information Processing Letters  53,</EM> 3 
	(February 1995), 145-152 (with D. Gries).
<li>Refinement for fault-tolerance:  An aircraft hand-off protocol.  
	<EM>Foundations of Ultradependable Parallel and Distributed Computing, 
	Paradigms for Dependable Applications,</EM> Kluwer Academic Publishers, 
	1994, 39-54 (with K. Marzullo and J. Dehn).
<li>Teaching logic as a tool. <EM>Proceedings 26th SIGCSE Technical Symposium 
	on Computer Science Education</EM>  (Nashville, Tennessee, March 1995), 
	<EM>SIGCSE Bulletin 27,</EM> 1, 384-385 (with D. Gries).
<li>Operating system support for mobile agents. <EM>Proceedings Fifth Workshop on 
	Hot Topics in Operating Systems HOTOS-V</EM>  (Orcas Island, Washington, 
	May 1995), 42-45 (with Dag Johansen and Robbert van Renesse).
<li>Verifying programs that use causally-ordered message-passing. <EM>Science of 
	Computer Programming  24,</EM> 2 (1995), 105-128 (with S. Stoller).
<li>On teaching proof.  <EM>Arts & Sciences NewsLetter  16,</EM> 2 (Spring 1995), 3  
	(with D. Gries).
<li>A new approach to discrete teaching mathematics. <EM>Primus V,</EM> 2 (June 1995), 
	113-138  (with D. Gries).
</ul>

<p>
<hr>
Return to: 
<dl>
<dt><!WA2><!WA2><!WA2><!WA2><IMG SRC="http://www.cs.cornell.edu/Icons/redball.gif"> 
	<!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/Department/Annual95/Beginning/annual-rpt95-home.html"> 
	1994-1995 Annual Report Home Page</a>
<dt><!WA4><!WA4><!WA4><!WA4><IMG SRC="http://www.cs.cornell.edu/Icons/redball.gif"> 
	<!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/"> 
	Departmental Home Page</a>
<p>
If you have questions or comments please contact:
<!WA6><!WA6><!WA6><!WA6><a href="mailto:www@cs.cornell.edu">www@cs.cornell.edu.</a>
<p>
<hr>
Last modified: 24 November 1995 by Denise Moore 
(denise@cs.cornell.edu).
</body>
</html>